\begin{tabbing} (\=with ds: ${\it ds}$\+ \\[0ex]action $a$:$T$ \\[0ex]precondition $a$(v) is \\[0ex]$P$ s v) \-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=mk{-}ma(${\it ds}$;\+ \\[0ex]locl($a$) : $T$; \\[0ex]; \\[0ex]$a$ : $P$; \\[0ex]; \\[0ex]; \\[0ex]; \\[0ex]; \\[0ex]; \\[0ex]; \\[0ex]) \- \end{tabbing}